$\forall$${\it es}$:ES, $A$:Type, ${\it Xs}$:(AbsInterface($A$) List).
\\[0ex]($\forall$$f$,$g$$\in$${\it Xs}$.  p{-}disjoint(E;$f$;$g$))
\\[0ex]$\Rightarrow$ ($\forall$$X$:AbsInterface($A$). ($X$ $\in$ ${\it Xs}$) $\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ (p{-}first(${\it Xs}$)($e$) = $X$($e$) $\in$ $A$)))